$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), ${\it finv}$:($B$$\rightarrow$(?$A$)). inv{-}rel($A$;$B$;$f$;${\it finv}$) $\Rightarrow$ Inj($A$;$B$;$f$)